∀e w123 RW w1 0;
taut A(RW,w1,W123,0) 61 89;
∀e initial3 RW w1;
taut color(W1,w1)=W ∧ color(W3,w1)=W 91 26 61;
taut color(W1,w1)=W ∧ color(W3,w1)=W 91 26 61 rw;
tauteq color(W1,w1)=W ∧ color(W3,w1)=W 91 26 61 rw;
exit;∀e initial1 B w1;
tauteq 93:#2#1#2 93 90 92;
∃e 94 w3;
tauteq ¬(95:#1 ⊃ color(W1,w3)=color(W1,w1)) 95 92 color1;
∃i 96 w3←w3;
unify ¬∀w3.97:#1#1 97;
show proof 60:↑ →prf;
show proof→wisema.prf;
show proof 78
;
taut 98:≡78: 98 78;
cancel;
taut 98:#1≡78:#1 78 98;
assume p=W1;
subst 100 in 99;
⊃i 100 99;
show proof 72;
tauteq p=W1⊃72:#2 102;
cancel;
⊃i 100 w01;
⊃i 100 101;
tauteq A(RW,w3,W123,0) ⊃ color(W123,w3)=color(W123,RW) 62 64;
∀i ↑ w3;
taut 66:≡104: 66 104;
assume p=W123;
subst 106 in 105;
⊃i 106 107;
show proof→wisema.prf;
show proof 102;
tauteq p=W1⊃108:#2 102;
tauteq 93:#2#2#2#2 90 92 93;
∃e 110 w3;
tauteq ¬(111:#1 ⊃ color(W3,w3)=color(W3,w1)) 111 92 color1;
∃i 112 w3←w3;
unify ¬∀.113:#1#1 113;
unify ¬∀w3.113:#1#1 113;
exit;show proof→wisema.prf;
show proof ↑;
show proof 88;
taut 114:#1≡88:#1 114 88;
assume p=W3;
subst 116 in 115;
⊃i 116 117;
tauteq p=W3⊃108:#2 118;
∀e initial1 W w1;
tauteq 120:#2#2#1#2 120 90;
∃e 121 w3;
tauteq ¬(122:#1 ⊃ color(W2,w3)= color(W2,w1)) 122 61 color1;
∃i 123 w3←w3;
unify ¬∀w3.124:#1#1 124;
show proof 83;
taut 125:#1≡83:#1 125 83;
assume p=W2;
subst 127 in 126;
⊃i 127 128;
tauteq p=W2⊃108:#2 129;
show axiom who;
show axioms who;
show axioms color;
axiom who: ∀p.(p=W1 ∨ p= W2 ∨ p=W3 ∨ p=W123);;
∀e who p;
taut 108:#2 108 109 119 130 131;
∀i 132 p;
exit;show proof→wisema.prf;
show proof ↑;
show proof 61;
∀e w123 RW w1;
cancel;
∀e w123 RW w1 0;
∀e elwek11 w1;
taut 135:#1 135 61 133 134;
cancel;
tauteq ¬(135:#1 ⊃ color(W2,w1)=color(W2,RW)) 135 61 133 134 rw color1;
∃i 136 w1←w1;
cancel;
∃i 136 w1←w;
unify ¬∀w.137:#1#1 137;
exit;show proof→wisema.
prf;
tauteq FALSE 55 ↑;
show proof ↑ 55;
fetch wise3.cmd;
show proof 136;
cancel 136;
∀e elwek13 RW w1;
tauteq ¬(A(RW,w1,W2,1)⊃color(W2,1)=color(W2,RW)) rw color1 61 133 135 136;
tauteq ¬(A(RW,w1,W2,1)⊃color(W2,w1)=color(W2,RW)) rw color1 61 133 135 136;
show proof 130:↑;
taut 135:#2#2≡133:;
cancel;
show proof 61;
show proof 133:↑;
tauteq ¬(A(RW,w1,W2,1)⊃color(W2,w1)=color(W2,RW)) 61 rw color1 133:136;
∃i 137 w1←w1;
unify ¬∀w1.138:#1#1 138;
taut FALSE 55 139;
¬i 140 2;
⊃i 1 ↑;
∀e color2 color(W3,w);
tauteq 142:#1 ⊃ color(W3,w)=color(W3,RW) 142 143 rw;
∀i 144 w;
show proof→wise3.prf;
exit;fetch sandp.ax;
exit;